k:Knd, T:Type, l:IdLnk, ds, dt:tg:Id fp Type,
g:(tg:Id(State(ds)T(DeclaredType(dt;tg) List))) List.
(isrcv(k)  lnk(k) = l  T = DeclaredType(dt;tag(k)))
 (isrcv(k)  destination(lnk(k)) = source(l)  Id)
 Normal(ds)
 Normal(T)
 Normal(dt)
 es.sends k(v:T) on l:
 es.tagged(g,State(ds),v):dt 

latex

Definitions

DeclaredType(ds;x), <a,b>, Type, s = t, P  Q, x:AB(x), t  T, x:A. B(x), isrcv(k), b, lnk(k), a = b, source(l), destination(l), Id, P & Q, Void, f(x)?z, ES, type List, State(ds), x:AB(x), IdDeq, x.A(x), x. t(x), S  T, S  T, sends k(v:T) on l:tagged(g,State(ds),v):dt, Prop, R ||- es.P(es), x:A. B(x), es.P(es), Knd, IdLnk, a:A fp B(a), tag(k), Normal(ds), Normal(T), sends knd(v:T) on l:tagged(g,State(ds),v):dt, P  Q

Lemmas

assert-eq-lnk, normal-type wf, normal-ds wf, ldst wf, lsrc wf, tagof wf, fpf wf, IdLnk wf, Knd wf, Rsends wf, R-realizes wf, sends-p wf, fpf-cap wf, id-deq wf, Id wf, decl-state wf, decl-type wf, event system wf, R-sends-rule, eq lnk wf, lnk wf, assert wf, isrcv wf